;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
(interface Icrop
  (sig trim-columns (oldRow firstCol lastCol))
  (sig crop (tr firstRow firstCol lastRow lastCol))
  
  ; contracts
  (con trim-columns-returns-row-list
       (implies (and (row-list? oldRow) (natp firstCol)
                     (natp lastCol) (<= firstCol lastCol)))
       (row-list? (trim-columns oldRow firstCol lastCol)))
       
  (con trim-columns-returns-correct-sized-row-list
       (implies (and (row-list? oldRow) (natp firstCol)
                     (natp lastCol) (<= firstCol lastCol)))
       (= (len (trim-columns oldRow firstCol lastCol))
          (+ (- lastCol firstCol) 1)))
  
  (con trim-columns-returns-correct-columns
       (implies (and (row-list? oldRow) (natp firstCol)
                     (natp lastCol) (<= firstCol lastCol)))
       (and (equal (cdar newlist) (cdr (nth firstCol rowlist)))  
            (equal (cdar (last newlist)) (cdr (nth lastCol 
                                                   rowlist))))) 
  
  ; verifies that crop returns a bmp-tree
  (con crop-returns-true-bmp-tree
       (implies (and (bmp-tree? tr) (natp firstRow)  
                     (natp lastRow) (<= firstRow lastRow)
                     (natp firstCol) (natp lastRow) 
                     (<= firstCol lastCol)))
       (true-bmp-tree? (crop tr firstRow firstCol lastRow lastCol)))
  
  ; verifies that crop returns a correct-sized bitmap
  (con crop-returns-correct-sized-bitmap
       (implies (and (bmp-tree? tr) (natp firstRow)  
                     (natp lastRow) (<= firstRow lastRow)
                     (natp firstCol) (natp lastRow) 
                     (<= firstCol lastCol)))
       (equal (get-dimensions 
               (crop tr firstRow firstCol lastRow lastCol))
              (cons (+ (- lastRow firstRow))
                    (+ (- lastCol firstCol)))))
  
  ; verifies that crop trims the bitmap to within the given pixels
  (con crop-returns-correct-subimage
       (implies (and (bmp-tree? tr) (natp firstRow)  
                     (natp lastRow) (<= firstRow lastRow)
                     (natp firstCol) (natp lastRow) 
                     (<= firstCol lastCol)))
       (and (equal (get-pixel-color (crop tr firstRow firstCol 
                                          lastRow lastCol) 0 0)
                   (get-pixel-color tr firstRow firstCol))
            (equal (get-pixel-color (crop tr firstRow firstCol 
                                          lastRow lastCol) 
                                    (- lastRow firstRow)
                                    (- lastCol firstCol))
                   (get-pixel-color tr lastRow lastCol))))
  )
